abs-fifo{i:l}(C;T)(es,In,Out)
== i:C.
== f:{e:E| abs-R (i,e)} {e:E| j:C. (abs-S (j,i,e))} 
== (e.j:C. (abs-S (j,i,e))  f e.abs-R (i,e)
== & (e:{e:E| abs-R (i,e)} , j:{j:C| abs-S (j,i,f(e))} . (Out(e).2) = (In(f(e)).2))
== & (e, e':{e:E| abs-R (i,e)} , j:C.
== & ((abs-S (j,i,f(e)))  (abs-S (j,i,f(e')))  f(e) c f(e')  e c e')) 

latex

---

clarification:

abs-fifo{i:l}(C; T)(es,In,Out)
== i:C.
== f:{e:es-E(es)| abs-R(C;Out)(i,e)} {e:es-E(es)| j:C. (abs-S(C;In)(j,i,e))} 
== (antecedent-surjection(es;e.abs-R(C;Out)(i,e);e.j:C. (abs-S(C;In)(j,i,e));f)
== & (e:{e:es-E(es)| abs-R(C;Out)(i,e)} , j:{j:C| abs-S(C;In)(j,i,f(e))} .
== & ((Out(e).2) = (In(f(e)).2)  T)
== & (e:{e:es-E(es)| abs-R(C;Out)(i,e)} , e':{e:es-E(es)| abs-R(C;Out)(i,e)} , j:C.
== & ((abs-S(C;In)(j,i,f(e)))
== & ( (abs-S(C;In)(j,i,f(e')))
== & ( es-causle(es;f(e);f(e'))
== & ( es-causle(es;e;e'))) 

latex

Definitions	x:AB(x), Q  f P, x.A(x), x:A. B(x), P & Q, s = t, t.2, X(e), {x:A| B(x)} , E, abs-R , x:A. B(x), abs-S , P  Q, f(a), e c e'
FDL editor aliases	abs-fifo